w:World, e, e':E. FairFifo  pred!(e;e')  time(e)<time(e') 

latex

Definitions

left+right, P  Q, pred!(e;e'), World, t  T, x:A. B(x), E, FairFifo, w-pred(w;e), x.A(x), P  Q, w-info(w;e), Id, time(e), a<b, , {x:A| B(x) }, x:AB(x), Prop, x:AB(x), A & B, True, b, isrcv(k), rcv(l,tg), {T}, SQType(T), Knd, s = t, s ~ t, False, Unit, , Type, sender(e), tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), ecase1(e;info;i.f(i);l,e'.g(l;e')), sender(e), rcv?(e), kind(e), P & Q, AB, i  j < k, match(l;t;t'), #$n, {i..j}, x:A. B(x), A, mu(f), , Dec(P)

Lemmas

mu wf, decidable le, w-match-exists, mu-property, le wf, assert wf, w-match wf, lnk wf, w-ekind wf, true wf, w-sender wf, false wf, it wf, Knd wf, Knd sq, w-pred-decreases, w-time wf, nat wf, pred! wf, Id wf, w-info wf, w-pred wf, fair-fifo wf, w-E wf, world wf